Realizer
== rec(X.Unit
== rec(X.+XX
== rec(X.+IdT:TypeIdT
== rec(X.+IdTypeId(Knd List)
== rec(X.+IdLnkId(Knd List)
== rec(X.+Idds:x:Id fp TypeKndT:Typex:Id(State(ds)TDeclaredType(ds;x))
== rec(X.+ds:x:Id fp Type
== rec(X.+Knd
== rec(X.+T:Type
== rec(X.+IdLnk
== rec(X.+dt:x:Id fp Type
== rec(X.+((tg:Id(State(ds)T(DeclaredType(dt;tg) List))) List)
== rec(X.+Idds:x:Id fp TypeIdT:Type(State(ds)TProp)
== rec(X.+IdKnd(Id List)
== rec(X.+IdKnd(IdLnk List)
== rec(X.+IdId(Knd List)) 

latex

---

clarification:

es_realizer{i:l}
== rec(X.Unit
== rec(X.+XX
== rec(X.+IdT:Type{i}IdT
== rec(X.+IdType{i}Id(Knd List)
== rec(X.+IdLnkId(Knd List)
== rec(X.+Idds:x:Id fp Type{i}KndT:Type{i}x:Id(State(ds)Tdecl-type{i:l}(ds; x))
== rec(X.+ds:x:Id fp Type{i}
== rec(X.+Knd
== rec(X.+T:Type{i}
== rec(X.+IdLnk
== rec(X.+dt:x:Id fp Type{i}
== rec(X.+((tg:Id(State(ds)T(decl-type{i:l}(dt; tg) List))) List)
== rec(X.+Idds:x:Id fp Type{i}IdT:Type{i}(State(ds)TProp{i})
== rec(X.+IdKnd(Id List)
== rec(X.+IdKnd(IdLnk List)
== rec(X.+IdId(Knd List)) 

latex

Definitions	rec(x.A(x)), Unit, DeclaredType(ds;x), a:A fp B(a), Type, State(ds), x:AB(x), Prop, left+right, IdLnk, x:AB(x), Id, type List, Knd
FDL editor aliases	es_realizer